g:IMonoid, n:, e:|g|. (n  e) = (((n - 1)  e) * e)  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, n x(op;id) e, n  e
Definitions	t  T, n x(op;id) e, n  e, x:A. B(x), x. t(x), IMonoid, x(s), P  Q,
Lemmas	imon wf, nat plus wf, grp car wf, int seg wf, itop unroll hi